package cfsmon.logic.dfm;

import java.util.HashMap;
import java.util.Map;

import cfsmon.common.Event;

/**
 * The state of a deterministic finite state machine. It consist of a name and outgoing
 * transitions. The transitions are modeled as a total function from events to target states.
 * The concept of a 'default transition' completes the transition function in the following
 * way: Every event that does not cause a transition into another state causes a transition
 * into the state denoted as default transition. Thus the value of the transition function is
 * defined for every event.
 * @author Alexander Gebhardt
 */
public class DfmState {

	private static int runningID = 0;
	private int id;
	private String name;
	private Map<Event, DfmState> transitions;
	private DfmState defaultTransition;
	
	public DfmState(){
		this(null);
	}
	
	public DfmState(String name){
		super();
		if (name == null){
			this.name = "d" + runningID;
		} else {
			this.name = name;			
		}
		this.id = runningID++;
		this.transitions = new HashMap<Event, DfmState>();
		defaultTransition = this;
	}
	
	public String getName() {
		return name;
	}
	
	public int getID(){
		return id;
	}
	
	/**
	 * Adds a transition from this state to a target state triggered by an event.
	 * @param e an event
	 * @param to the target state
	 * @throws IllegalArgumentException if at least one parameter is null
	 */
	public void putTransition(Event e, DfmState to) throws IllegalArgumentException{
		if (e == null || to == null)
			throw new IllegalArgumentException("Invalid parameters to putTransition call of a state");
		transitions.put(e, to);
	}
	
	public Map<Event, DfmState> getTransitions(){
		return transitions;
	}
	
	public DfmState getDefaultTransition(){
		return defaultTransition;
	}
	
	public void setDefaultTransition(DfmState t) throws IllegalArgumentException{
		if (t == null)
			throw new IllegalArgumentException("Invalid parameters to addDefaultTransition call of a state");
		defaultTransition = t;
	}
	
	@Override
	public String toString(){
		return name;
	}
	
	public void printDeep(){
		
		for (Event e : transitions.keySet()){
			System.out.println("(" + this + ", " + e + ", " + transitions.get(e) + ") in Delta");
			
		}
		System.out.println("forall e in Events. NEx s in States where delta(" + this + ", e) = s implies delta'("+ this + ", e) = " + defaultTransition);
		
	}
	
}
